k:Knd, T, B:Type, l:IdLnk, ds:x:Id fp Type, tg:Id, f:(State(ds)TB).
(isrcv(k)  destination(lnk(k)) = source(l)  Id & (lnk(k) = l  T = B & tag(k) = tg))
 Normal(ds)
 Normal(T)
 Normal(B)
 sends k(v:T) on l:
 tagged([<tg,s,v. [f(s,v)]>],State(ds),v):tg : B
 ||- es.usends1-p(es;ds;k;T;l;tg;B;f) 

latex

Definitions

Top, x. t(x), Prop, t  T, P & Q, e@i. P(e), x:A. B(x), P  Q, x:A. B(x), A & B, false, true, if b t else f fi, f(x)?z, 2of(t), f(x), x : v, Y, ||as||, False, A, AB, ij, x(s), map(f;as), {T}, Unit, , P  Q, hd(l),

Lemmas

usends1-p wf, event system wf, fpf-cap wf, id-deq wf, fpf-cap-single1, sends-p wf, Rsends wf, R-implies-rule, es-E wf, lsrc wf, es-loc wf, es-kind wf, Knd wf, rcv wf, es-sender wf, es-kind-rcv, equal functionality wrt subtype rel, subtype rel list, subtype rel self, subtype rel product, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, top wf, fpf-single wf, fpf-dom wf, length wf1, hd wf, pi2 wf, es-val wf